FDL - Step of Proof: p-fun-exp-injection

Step of Proof: p-fun-exp-injection

Inference at * 2
Iof proof for Lemma p-fun-exp-injection:

.....upcase..... NILNIL

1. A : Type
2. f : A

(A + Top)
3. p-inject(A;A;f)
4. n :

5. 0 < n
6. p-inject(A;A;f^n - 1)

p-inject(A;A;f^n)

by ((Unfold `p-fun-exp` ( 0)

)

CollapseTHEN (((RecUnfold `primrec` 0)

CollapseTHEN ((((((if (0

C) =0 then SplitOnConclITE else SplitOnHypITE (0))

)
CollapseTHENA (Auto

))

)
CCollapseTHEN (((
CC(Try ((Complete (Auto'))

))

)
CCollapseTHEN (((Fold `p-fun-exp` 0)
CCollapseTHEN (((Reduce 0)

CCoCollapseTHEN (((BLemma `p-compose-inject`)
CCollapseTHEN (Auto

))

))

))

))

))

))

))

CC.

Definitions left + right, Unit, i z j, i <z j, p q, p q, p q, [d], a < b, x f y, a < b, null(as), x =a y, P Q, P & Q, x:A B(x), tt, b, , (i = j), ff, b, f(a), primrec(n;b;c), p-id(), x.A(x), f o g , , {x:A| B(x)} , False, P Q, Void, n+m, -n, x:A. B(x), x:AB(x), , Type, A B, s = t, t T, A, f^n, n - m, #$n, a < b, p-inject(A;B;f),

Lemmas eqtt to assert, eqff to assert, iff transitivity, assert of bnot, not functionality wrt iff, assert of eq int, eq int wf, bool wf, bnot wf, not wf, assert wf, p-inject wf, p-compose-inject, p-fun-exp wf, nat wf, member wf, le wf